|
In proof theory, proof nets are a geometrical method of representing proofs that eliminates two forms of ''bureaucracy'' that differentiates proofs: (A) irrelevant syntactical features of regular proof calculi such as the natural deduction calculus and the sequent calculus, and (B) the order of rules applied in a derivation. In this way, the formal properties of proof identity correspond more closely to the intuitively desirable properties. Proof nets were introduced by Jean-Yves Girard. For instance, these two linear logic proofs are “morally” identical: |} And their corresponding nets will be the same. == Correctness criteria == Several correctness criteria are known to check if a sequential proof structure (i.e. something which seems to be a proof net) is actually a concrete proof structure (i.e. something which encodes a valid derivation in linear logic). The first such criterion is the long-trip criterion〔Girard, Jean-Yves. ''(Linear logic )'', Theoretical Computer Science, Vol 50, no 1, pp. 1–102, 1987〕 which was described by Jean-Yves Girard. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「proof net」の詳細全文を読む スポンサード リンク
|